Left Termination proof of /tmp/tmpIpm3Ru/ways.pl

Left Termination of the query pattern ways_in_3(g, g, a) w.r.t. the given Prolog program could not be shown:

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

Clauses:

nat(0).
nat(s(X)) :- nat(X).
plus(0, X, X) :- nat(X).
plus(s(X), Y, s(Z)) :- plus(X, Y, Z).
ways(0, _, s(0)).
ways(_, [], 0).
ways(Amount, .(s(C), Coins), N) :- ','(=(Amount, s(_)), ','(plus(s(C), NewAmount, Amount), ','(ways(Amount, Coins, N1), ','(ways(NewAmount, .(s(C), Coins), N2), plus(N1, N2, N))))).
ways(Amount, .(s(C), Coins), N) :- ','(=(Amount, s(_)), ','(plus(Amount, s(_), s(C)), ways(Amount, Coins, N))).

Queries:

ways(g,g,a).

Added definitions of predefined predicates.

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

Clauses:

nat(0).
nat(s(X)) :- nat(X).
plus(0, X, X) :- nat(X).
plus(s(X), Y, s(Z)) :- plus(X, Y, Z).
ways(0, X, s(0)).
ways(X, [], 0).
ways(Amount, .(s(C), Coins), N) :- ','(=(Amount, s(X)), ','(plus(s(C), NewAmount, Amount), ','(ways(Amount, Coins, N1), ','(ways(NewAmount, .(s(C), Coins), N2), plus(N1, N2, N))))).
ways(Amount, .(s(C), Coins), N) :- ','(=(Amount, s(X)), ','(plus(Amount, s(X1), s(C)), ways(Amount, Coins, N))).
=(X, X).

Queries:

ways(g,g,a).

We use the technique of [30].Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

ways_in(Amount, .(s(C), Coins), N) → U4(Amount, C, Coins, N, =_in(Amount, s(X)))
=_in(X, X) → =_out(X, X)
U4(Amount, C, Coins, N, =_out(Amount, s(X))) → U9(Amount, C, Coins, N, X, plus_in(Amount, s(X1), s(C)))
plus_in(s(X), Y, s(Z)) → U3(X, Y, Z, plus_in(X, Y, Z))
plus_in(0, X, X) → U2(X, nat_in(X))
nat_in(s(X)) → U1(X, nat_in(X))
nat_in(0) → nat_out(0)
U1(X, nat_out(X)) → nat_out(s(X))
U2(X, nat_out(X)) → plus_out(0, X, X)
U3(X, Y, Z, plus_out(X, Y, Z)) → plus_out(s(X), Y, s(Z))
U9(Amount, C, Coins, N, X, plus_out(Amount, s(X1), s(C))) → U10(Amount, C, Coins, N, ways_in(Amount, Coins, N))
ways_in(X, [], 0) → ways_out(X, [], 0)
ways_in(0, X, s(0)) → ways_out(0, X, s(0))
U10(Amount, C, Coins, N, ways_out(Amount, Coins, N)) → ways_out(Amount, .(s(C), Coins), N)
U4(Amount, C, Coins, N, =_out(Amount, s(X))) → U5(Amount, C, Coins, N, X, plus_in(s(C), NewAmount, Amount))
U5(Amount, C, Coins, N, X, plus_out(s(C), NewAmount, Amount)) → U6(Amount, C, Coins, N, X, NewAmount, ways_in(Amount, Coins, N1))
U6(Amount, C, Coins, N, X, NewAmount, ways_out(Amount, Coins, N1)) → U7(Amount, C, Coins, N, X, NewAmount, N1, ways_in(NewAmount, .(s(C), Coins), N2))
U7(Amount, C, Coins, N, X, NewAmount, N1, ways_out(NewAmount, .(s(C), Coins), N2)) → U8(Amount, C, Coins, N, plus_in(N1, N2, N))
U8(Amount, C, Coins, N, plus_out(N1, N2, N)) → ways_out(Amount, .(s(C), Coins), N)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

ways_in(Amount, .(s(C), Coins), N) → U4(Amount, C, Coins, N, =_in(Amount, s(X)))
=_in(X, X) → =_out(X, X)
U4(Amount, C, Coins, N, =_out(Amount, s(X))) → U9(Amount, C, Coins, N, X, plus_in(Amount, s(X1), s(C)))
plus_in(s(X), Y, s(Z)) → U3(X, Y, Z, plus_in(X, Y, Z))
plus_in(0, X, X) → U2(X, nat_in(X))
nat_in(s(X)) → U1(X, nat_in(X))
nat_in(0) → nat_out(0)
U1(X, nat_out(X)) → nat_out(s(X))
U2(X, nat_out(X)) → plus_out(0, X, X)
U3(X, Y, Z, plus_out(X, Y, Z)) → plus_out(s(X), Y, s(Z))
U9(Amount, C, Coins, N, X, plus_out(Amount, s(X1), s(C))) → U10(Amount, C, Coins, N, ways_in(Amount, Coins, N))
ways_in(X, [], 0) → ways_out(X, [], 0)
ways_in(0, X, s(0)) → ways_out(0, X, s(0))
U10(Amount, C, Coins, N, ways_out(Amount, Coins, N)) → ways_out(Amount, .(s(C), Coins), N)
U4(Amount, C, Coins, N, =_out(Amount, s(X))) → U5(Amount, C, Coins, N, X, plus_in(s(C), NewAmount, Amount))
U5(Amount, C, Coins, N, X, plus_out(s(C), NewAmount, Amount)) → U6(Amount, C, Coins, N, X, NewAmount, ways_in(Amount, Coins, N1))
U6(Amount, C, Coins, N, X, NewAmount, ways_out(Amount, Coins, N1)) → U7(Amount, C, Coins, N, X, NewAmount, N1, ways_in(NewAmount, .(s(C), Coins), N2))
U7(Amount, C, Coins, N, X, NewAmount, N1, ways_out(NewAmount, .(s(C), Coins), N2)) → U8(Amount, C, Coins, N, plus_in(N1, N2, N))
U8(Amount, C, Coins, N, plus_out(N1, N2, N)) → ways_out(Amount, .(s(C), Coins), N)

WAYS_IN(Amount, .(s(C), Coins), N) → U4¹(Amount, C, Coins, N, =_in(Amount, s(X)))
WAYS_IN(Amount, .(s(C), Coins), N) → =_IN(Amount, s(X))
U4¹(Amount, C, Coins, N, =_out(Amount, s(X))) → U9¹(Amount, C, Coins, N, X, plus_in(Amount, s(X1), s(C)))
U4¹(Amount, C, Coins, N, =_out(Amount, s(X))) → PLUS_IN(Amount, s(X1), s(C))
PLUS_IN(s(X), Y, s(Z)) → U3¹(X, Y, Z, plus_in(X, Y, Z))
PLUS_IN(s(X), Y, s(Z)) → PLUS_IN(X, Y, Z)
PLUS_IN(0, X, X) → U2¹(X, nat_in(X))
PLUS_IN(0, X, X) → NAT_IN(X)
NAT_IN(s(X)) → U1¹(X, nat_in(X))
NAT_IN(s(X)) → NAT_IN(X)
U9¹(Amount, C, Coins, N, X, plus_out(Amount, s(X1), s(C))) → U10¹(Amount, C, Coins, N, ways_in(Amount, Coins, N))
U9¹(Amount, C, Coins, N, X, plus_out(Amount, s(X1), s(C))) → WAYS_IN(Amount, Coins, N)
U4¹(Amount, C, Coins, N, =_out(Amount, s(X))) → U5¹(Amount, C, Coins, N, X, plus_in(s(C), NewAmount, Amount))
U4¹(Amount, C, Coins, N, =_out(Amount, s(X))) → PLUS_IN(s(C), NewAmount, Amount)
U5¹(Amount, C, Coins, N, X, plus_out(s(C), NewAmount, Amount)) → U6¹(Amount, C, Coins, N, X, NewAmount, ways_in(Amount, Coins, N1))
U5¹(Amount, C, Coins, N, X, plus_out(s(C), NewAmount, Amount)) → WAYS_IN(Amount, Coins, N1)
U6¹(Amount, C, Coins, N, X, NewAmount, ways_out(Amount, Coins, N1)) → U7¹(Amount, C, Coins, N, X, NewAmount, N1, ways_in(NewAmount, .(s(C), Coins), N2))
U6¹(Amount, C, Coins, N, X, NewAmount, ways_out(Amount, Coins, N1)) → WAYS_IN(NewAmount, .(s(C), Coins), N2)
U7¹(Amount, C, Coins, N, X, NewAmount, N1, ways_out(NewAmount, .(s(C), Coins), N2)) → U8¹(Amount, C, Coins, N, plus_in(N1, N2, N))
U7¹(Amount, C, Coins, N, X, NewAmount, N1, ways_out(NewAmount, .(s(C), Coins), N2)) → PLUS_IN(N1, N2, N)

The TRS R consists of the following rules:

ways_in(Amount, .(s(C), Coins), N) → U4(Amount, C, Coins, N, =_in(Amount, s(X)))
=_in(X, X) → =_out(X, X)
U4(Amount, C, Coins, N, =_out(Amount, s(X))) → U9(Amount, C, Coins, N, X, plus_in(Amount, s(X1), s(C)))
plus_in(s(X), Y, s(Z)) → U3(X, Y, Z, plus_in(X, Y, Z))
plus_in(0, X, X) → U2(X, nat_in(X))
nat_in(s(X)) → U1(X, nat_in(X))
nat_in(0) → nat_out(0)
U1(X, nat_out(X)) → nat_out(s(X))
U2(X, nat_out(X)) → plus_out(0, X, X)
U3(X, Y, Z, plus_out(X, Y, Z)) → plus_out(s(X), Y, s(Z))
U9(Amount, C, Coins, N, X, plus_out(Amount, s(X1), s(C))) → U10(Amount, C, Coins, N, ways_in(Amount, Coins, N))
ways_in(X, [], 0) → ways_out(X, [], 0)
ways_in(0, X, s(0)) → ways_out(0, X, s(0))
U10(Amount, C, Coins, N, ways_out(Amount, Coins, N)) → ways_out(Amount, .(s(C), Coins), N)
U4(Amount, C, Coins, N, =_out(Amount, s(X))) → U5(Amount, C, Coins, N, X, plus_in(s(C), NewAmount, Amount))
U5(Amount, C, Coins, N, X, plus_out(s(C), NewAmount, Amount)) → U6(Amount, C, Coins, N, X, NewAmount, ways_in(Amount, Coins, N1))
U6(Amount, C, Coins, N, X, NewAmount, ways_out(Amount, Coins, N1)) → U7(Amount, C, Coins, N, X, NewAmount, N1, ways_in(NewAmount, .(s(C), Coins), N2))
U7(Amount, C, Coins, N, X, NewAmount, N1, ways_out(NewAmount, .(s(C), Coins), N2)) → U8(Amount, C, Coins, N, plus_in(N1, N2, N))
U8(Amount, C, Coins, N, plus_out(N1, N2, N)) → ways_out(Amount, .(s(C), Coins), N)

The argument filtering Pi contains the following mapping:
ways_in(x1, x2, x3) = ways_in(x1, x2)
.(x1, x2) = .(x1, x2)
s(x1) = s(x1)
U4(x1, x2, x3, x4, x5) = U4(x1, x2, x3, x5)
=_in(x1, x2) = =_in(x1)
=_out(x1, x2) = =_out(x1, x2)
U9(x1, x2, x3, x4, x5, x6) = U9(x1, x2, x3, x6)
plus_in(x1, x2, x3) = plus_in(x1)
U3(x1, x2, x3, x4) = U3(x1, x4)
0 = 0
U2(x1, x2) = U2(x2)
nat_in(x1) = nat_in
U1(x1, x2) = U1(x2)
nat_out(x1) = nat_out(x1)
plus_out(x1, x2, x3) = plus_out(x1, x2, x3)
U10(x1, x2, x3, x4, x5) = U10(x1, x2, x3, x5)
[] = []
ways_out(x1, x2, x3) = ways_out(x1, x2, x3)
U5(x1, x2, x3, x4, x5, x6) = U5(x1, x2, x3, x6)
U6(x1, x2, x3, x4, x5, x6, x7) = U6(x1, x2, x3, x6, x7)
U7(x1, x2, x3, x4, x5, x6, x7, x8) = U7(x1, x2, x3, x7, x8)
U8(x1, x2, x3, x4, x5) = U8(x1, x2, x3, x5)
U5¹(x1, x2, x3, x4, x5, x6) = U5¹(x1, x2, x3, x6)
U7¹(x1, x2, x3, x4, x5, x6, x7, x8) = U7¹(x1, x2, x3, x7, x8)
PLUS_IN(x1, x2, x3) = PLUS_IN(x1)
U2¹(x1, x2) = U2¹(x2)
U6¹(x1, x2, x3, x4, x5, x6, x7) = U6¹(x1, x2, x3, x6, x7)
=_IN(x1, x2) = =_IN(x1)
U10¹(x1, x2, x3, x4, x5) = U10¹(x1, x2, x3, x5)
U3¹(x1, x2, x3, x4) = U3¹(x1, x4)
U4¹(x1, x2, x3, x4, x5) = U4¹(x1, x2, x3, x5)
U9¹(x1, x2, x3, x4, x5, x6) = U9¹(x1, x2, x3, x6)
U1¹(x1, x2) = U1¹(x2)
U8¹(x1, x2, x3, x4, x5) = U8¹(x1, x2, x3, x5)
WAYS_IN(x1, x2, x3) = WAYS_IN(x1, x2)
NAT_IN(x1) = NAT_IN

We have to consider all (P,R,Pi)-chains

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

WAYS_IN(Amount, .(s(C), Coins), N) → U4¹(Amount, C, Coins, N, =_in(Amount, s(X)))
WAYS_IN(Amount, .(s(C), Coins), N) → =_IN(Amount, s(X))
U4¹(Amount, C, Coins, N, =_out(Amount, s(X))) → U9¹(Amount, C, Coins, N, X, plus_in(Amount, s(X1), s(C)))
U4¹(Amount, C, Coins, N, =_out(Amount, s(X))) → PLUS_IN(Amount, s(X1), s(C))
PLUS_IN(s(X), Y, s(Z)) → U3¹(X, Y, Z, plus_in(X, Y, Z))
PLUS_IN(s(X), Y, s(Z)) → PLUS_IN(X, Y, Z)
PLUS_IN(0, X, X) → U2¹(X, nat_in(X))
PLUS_IN(0, X, X) → NAT_IN(X)
NAT_IN(s(X)) → U1¹(X, nat_in(X))
NAT_IN(s(X)) → NAT_IN(X)
U9¹(Amount, C, Coins, N, X, plus_out(Amount, s(X1), s(C))) → U10¹(Amount, C, Coins, N, ways_in(Amount, Coins, N))
U9¹(Amount, C, Coins, N, X, plus_out(Amount, s(X1), s(C))) → WAYS_IN(Amount, Coins, N)
U4¹(Amount, C, Coins, N, =_out(Amount, s(X))) → U5¹(Amount, C, Coins, N, X, plus_in(s(C), NewAmount, Amount))
U4¹(Amount, C, Coins, N, =_out(Amount, s(X))) → PLUS_IN(s(C), NewAmount, Amount)
U5¹(Amount, C, Coins, N, X, plus_out(s(C), NewAmount, Amount)) → U6¹(Amount, C, Coins, N, X, NewAmount, ways_in(Amount, Coins, N1))
U5¹(Amount, C, Coins, N, X, plus_out(s(C), NewAmount, Amount)) → WAYS_IN(Amount, Coins, N1)
U6¹(Amount, C, Coins, N, X, NewAmount, ways_out(Amount, Coins, N1)) → U7¹(Amount, C, Coins, N, X, NewAmount, N1, ways_in(NewAmount, .(s(C), Coins), N2))
U6¹(Amount, C, Coins, N, X, NewAmount, ways_out(Amount, Coins, N1)) → WAYS_IN(NewAmount, .(s(C), Coins), N2)
U7¹(Amount, C, Coins, N, X, NewAmount, N1, ways_out(NewAmount, .(s(C), Coins), N2)) → U8¹(Amount, C, Coins, N, plus_in(N1, N2, N))
U7¹(Amount, C, Coins, N, X, NewAmount, N1, ways_out(NewAmount, .(s(C), Coins), N2)) → PLUS_IN(N1, N2, N)

The TRS R consists of the following rules:

ways_in(Amount, .(s(C), Coins), N) → U4(Amount, C, Coins, N, =_in(Amount, s(X)))
=_in(X, X) → =_out(X, X)
U4(Amount, C, Coins, N, =_out(Amount, s(X))) → U9(Amount, C, Coins, N, X, plus_in(Amount, s(X1), s(C)))
plus_in(s(X), Y, s(Z)) → U3(X, Y, Z, plus_in(X, Y, Z))
plus_in(0, X, X) → U2(X, nat_in(X))
nat_in(s(X)) → U1(X, nat_in(X))
nat_in(0) → nat_out(0)
U1(X, nat_out(X)) → nat_out(s(X))
U2(X, nat_out(X)) → plus_out(0, X, X)
U3(X, Y, Z, plus_out(X, Y, Z)) → plus_out(s(X), Y, s(Z))
U9(Amount, C, Coins, N, X, plus_out(Amount, s(X1), s(C))) → U10(Amount, C, Coins, N, ways_in(Amount, Coins, N))
ways_in(X, [], 0) → ways_out(X, [], 0)
ways_in(0, X, s(0)) → ways_out(0, X, s(0))
U10(Amount, C, Coins, N, ways_out(Amount, Coins, N)) → ways_out(Amount, .(s(C), Coins), N)
U4(Amount, C, Coins, N, =_out(Amount, s(X))) → U5(Amount, C, Coins, N, X, plus_in(s(C), NewAmount, Amount))
U5(Amount, C, Coins, N, X, plus_out(s(C), NewAmount, Amount)) → U6(Amount, C, Coins, N, X, NewAmount, ways_in(Amount, Coins, N1))
U6(Amount, C, Coins, N, X, NewAmount, ways_out(Amount, Coins, N1)) → U7(Amount, C, Coins, N, X, NewAmount, N1, ways_in(NewAmount, .(s(C), Coins), N2))
U7(Amount, C, Coins, N, X, NewAmount, N1, ways_out(NewAmount, .(s(C), Coins), N2)) → U8(Amount, C, Coins, N, plus_in(N1, N2, N))
U8(Amount, C, Coins, N, plus_out(N1, N2, N)) → ways_out(Amount, .(s(C), Coins), N)

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ PiDP

                    ↳ UsableRulesProof

                  ↳ PiDP

                  ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

NAT_IN(s(X)) → NAT_IN(X)

The TRS R consists of the following rules:

ways_in(Amount, .(s(C), Coins), N) → U4(Amount, C, Coins, N, =_in(Amount, s(X)))
=_in(X, X) → =_out(X, X)
U4(Amount, C, Coins, N, =_out(Amount, s(X))) → U9(Amount, C, Coins, N, X, plus_in(Amount, s(X1), s(C)))
plus_in(s(X), Y, s(Z)) → U3(X, Y, Z, plus_in(X, Y, Z))
plus_in(0, X, X) → U2(X, nat_in(X))
nat_in(s(X)) → U1(X, nat_in(X))
nat_in(0) → nat_out(0)
U1(X, nat_out(X)) → nat_out(s(X))
U2(X, nat_out(X)) → plus_out(0, X, X)
U3(X, Y, Z, plus_out(X, Y, Z)) → plus_out(s(X), Y, s(Z))
U9(Amount, C, Coins, N, X, plus_out(Amount, s(X1), s(C))) → U10(Amount, C, Coins, N, ways_in(Amount, Coins, N))
ways_in(X, [], 0) → ways_out(X, [], 0)
ways_in(0, X, s(0)) → ways_out(0, X, s(0))
U10(Amount, C, Coins, N, ways_out(Amount, Coins, N)) → ways_out(Amount, .(s(C), Coins), N)
U4(Amount, C, Coins, N, =_out(Amount, s(X))) → U5(Amount, C, Coins, N, X, plus_in(s(C), NewAmount, Amount))
U5(Amount, C, Coins, N, X, plus_out(s(C), NewAmount, Amount)) → U6(Amount, C, Coins, N, X, NewAmount, ways_in(Amount, Coins, N1))
U6(Amount, C, Coins, N, X, NewAmount, ways_out(Amount, Coins, N1)) → U7(Amount, C, Coins, N, X, NewAmount, N1, ways_in(NewAmount, .(s(C), Coins), N2))
U7(Amount, C, Coins, N, X, NewAmount, N1, ways_out(NewAmount, .(s(C), Coins), N2)) → U8(Amount, C, Coins, N, plus_in(N1, N2, N))
U8(Amount, C, Coins, N, plus_out(N1, N2, N)) → ways_out(Amount, .(s(C), Coins), N)

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ PiDP

                    ↳ UsableRulesProof

                      ↳ PiDP

                        ↳ PiDPToQDPProof

                  ↳ PiDP

                  ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

NAT_IN(s(X)) → NAT_IN(X)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
NAT_IN(x1) = NAT_IN

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ PiDP

                    ↳ UsableRulesProof

                      ↳ PiDP

                        ↳ PiDPToQDPProof

                          ↳ QDP

                            ↳ NonTerminationProof

                  ↳ PiDP

                  ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

NAT_IN → NAT_IN

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

The TRS P consists of the following rules:

NAT_IN → NAT_IN

The TRS R consists of the following rules:none

s = NAT_IN evaluates to t =NAT_IN

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [ ]
Matcher: [ ]

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from NAT_IN to NAT_IN.

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ PiDP

                  ↳ PiDP

                    ↳ UsableRulesProof

                  ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

PLUS_IN(s(X), Y, s(Z)) → PLUS_IN(X, Y, Z)

The TRS R consists of the following rules:

ways_in(Amount, .(s(C), Coins), N) → U4(Amount, C, Coins, N, =_in(Amount, s(X)))
=_in(X, X) → =_out(X, X)
U4(Amount, C, Coins, N, =_out(Amount, s(X))) → U9(Amount, C, Coins, N, X, plus_in(Amount, s(X1), s(C)))
plus_in(s(X), Y, s(Z)) → U3(X, Y, Z, plus_in(X, Y, Z))
plus_in(0, X, X) → U2(X, nat_in(X))
nat_in(s(X)) → U1(X, nat_in(X))
nat_in(0) → nat_out(0)
U1(X, nat_out(X)) → nat_out(s(X))
U2(X, nat_out(X)) → plus_out(0, X, X)
U3(X, Y, Z, plus_out(X, Y, Z)) → plus_out(s(X), Y, s(Z))
U9(Amount, C, Coins, N, X, plus_out(Amount, s(X1), s(C))) → U10(Amount, C, Coins, N, ways_in(Amount, Coins, N))
ways_in(X, [], 0) → ways_out(X, [], 0)
ways_in(0, X, s(0)) → ways_out(0, X, s(0))
U10(Amount, C, Coins, N, ways_out(Amount, Coins, N)) → ways_out(Amount, .(s(C), Coins), N)
U4(Amount, C, Coins, N, =_out(Amount, s(X))) → U5(Amount, C, Coins, N, X, plus_in(s(C), NewAmount, Amount))
U5(Amount, C, Coins, N, X, plus_out(s(C), NewAmount, Amount)) → U6(Amount, C, Coins, N, X, NewAmount, ways_in(Amount, Coins, N1))
U6(Amount, C, Coins, N, X, NewAmount, ways_out(Amount, Coins, N1)) → U7(Amount, C, Coins, N, X, NewAmount, N1, ways_in(NewAmount, .(s(C), Coins), N2))
U7(Amount, C, Coins, N, X, NewAmount, N1, ways_out(NewAmount, .(s(C), Coins), N2)) → U8(Amount, C, Coins, N, plus_in(N1, N2, N))
U8(Amount, C, Coins, N, plus_out(N1, N2, N)) → ways_out(Amount, .(s(C), Coins), N)

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ PiDP

                  ↳ PiDP

                    ↳ UsableRulesProof

                      ↳ PiDP

                        ↳ PiDPToQDPProof

                  ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

PLUS_IN(s(X), Y, s(Z)) → PLUS_IN(X, Y, Z)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
PLUS_IN(x1, x2, x3) = PLUS_IN(x1)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ PiDP

                  ↳ PiDP

                    ↳ UsableRulesProof

                      ↳ PiDP

                        ↳ PiDPToQDPProof

                          ↳ QDP

                            ↳ QDPSizeChangeProof

                  ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

PLUS_IN(s(X)) → PLUS_IN(X)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

PLUS_IN(s(X)) → PLUS_IN(X)
The graph contains the following edges 1 > 1

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                    ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

U9¹(Amount, C, Coins, N, X, plus_out(Amount, s(X1), s(C))) → WAYS_IN(Amount, Coins, N)
U4¹(Amount, C, Coins, N, =_out(Amount, s(X))) → U9¹(Amount, C, Coins, N, X, plus_in(Amount, s(X1), s(C)))
U5¹(Amount, C, Coins, N, X, plus_out(s(C), NewAmount, Amount)) → U6¹(Amount, C, Coins, N, X, NewAmount, ways_in(Amount, Coins, N1))
WAYS_IN(Amount, .(s(C), Coins), N) → U4¹(Amount, C, Coins, N, =_in(Amount, s(X)))
U5¹(Amount, C, Coins, N, X, plus_out(s(C), NewAmount, Amount)) → WAYS_IN(Amount, Coins, N1)
U4¹(Amount, C, Coins, N, =_out(Amount, s(X))) → U5¹(Amount, C, Coins, N, X, plus_in(s(C), NewAmount, Amount))
U6¹(Amount, C, Coins, N, X, NewAmount, ways_out(Amount, Coins, N1)) → WAYS_IN(NewAmount, .(s(C), Coins), N2)

The TRS R consists of the following rules:

ways_in(Amount, .(s(C), Coins), N) → U4(Amount, C, Coins, N, =_in(Amount, s(X)))
=_in(X, X) → =_out(X, X)
U4(Amount, C, Coins, N, =_out(Amount, s(X))) → U9(Amount, C, Coins, N, X, plus_in(Amount, s(X1), s(C)))
plus_in(s(X), Y, s(Z)) → U3(X, Y, Z, plus_in(X, Y, Z))
plus_in(0, X, X) → U2(X, nat_in(X))
nat_in(s(X)) → U1(X, nat_in(X))
nat_in(0) → nat_out(0)
U1(X, nat_out(X)) → nat_out(s(X))
U2(X, nat_out(X)) → plus_out(0, X, X)
U3(X, Y, Z, plus_out(X, Y, Z)) → plus_out(s(X), Y, s(Z))
U9(Amount, C, Coins, N, X, plus_out(Amount, s(X1), s(C))) → U10(Amount, C, Coins, N, ways_in(Amount, Coins, N))
ways_in(X, [], 0) → ways_out(X, [], 0)
ways_in(0, X, s(0)) → ways_out(0, X, s(0))
U10(Amount, C, Coins, N, ways_out(Amount, Coins, N)) → ways_out(Amount, .(s(C), Coins), N)
U4(Amount, C, Coins, N, =_out(Amount, s(X))) → U5(Amount, C, Coins, N, X, plus_in(s(C), NewAmount, Amount))
U5(Amount, C, Coins, N, X, plus_out(s(C), NewAmount, Amount)) → U6(Amount, C, Coins, N, X, NewAmount, ways_in(Amount, Coins, N1))
U6(Amount, C, Coins, N, X, NewAmount, ways_out(Amount, Coins, N1)) → U7(Amount, C, Coins, N, X, NewAmount, N1, ways_in(NewAmount, .(s(C), Coins), N2))
U7(Amount, C, Coins, N, X, NewAmount, N1, ways_out(NewAmount, .(s(C), Coins), N2)) → U8(Amount, C, Coins, N, plus_in(N1, N2, N))
U8(Amount, C, Coins, N, plus_out(N1, N2, N)) → ways_out(Amount, .(s(C), Coins), N)

The argument filtering Pi contains the following mapping:
ways_in(x1, x2, x3) = ways_in(x1, x2)
.(x1, x2) = .(x1, x2)
s(x1) = s(x1)
U4(x1, x2, x3, x4, x5) = U4(x1, x2, x3, x5)
=_in(x1, x2) = =_in(x1)
=_out(x1, x2) = =_out(x1, x2)
U9(x1, x2, x3, x4, x5, x6) = U9(x1, x2, x3, x6)
plus_in(x1, x2, x3) = plus_in(x1)
U3(x1, x2, x3, x4) = U3(x1, x4)
0 = 0
U2(x1, x2) = U2(x2)
nat_in(x1) = nat_in
U1(x1, x2) = U1(x2)
nat_out(x1) = nat_out(x1)
plus_out(x1, x2, x3) = plus_out(x1, x2, x3)
U10(x1, x2, x3, x4, x5) = U10(x1, x2, x3, x5)
[] = []
ways_out(x1, x2, x3) = ways_out(x1, x2, x3)
U5(x1, x2, x3, x4, x5, x6) = U5(x1, x2, x3, x6)
U6(x1, x2, x3, x4, x5, x6, x7) = U6(x1, x2, x3, x6, x7)
U7(x1, x2, x3, x4, x5, x6, x7, x8) = U7(x1, x2, x3, x7, x8)
U8(x1, x2, x3, x4, x5) = U8(x1, x2, x3, x5)
U5¹(x1, x2, x3, x4, x5, x6) = U5¹(x1, x2, x3, x6)
U6¹(x1, x2, x3, x4, x5, x6, x7) = U6¹(x1, x2, x3, x6, x7)
U4¹(x1, x2, x3, x4, x5) = U4¹(x1, x2, x3, x5)
U9¹(x1, x2, x3, x4, x5, x6) = U9¹(x1, x2, x3, x6)
WAYS_IN(x1, x2, x3) = WAYS_IN(x1, x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

U9¹(Amount, C, Coins, plus_out(Amount, s(X1), s(C))) → WAYS_IN(Amount, Coins)
U6¹(Amount, C, Coins, NewAmount, ways_out(Amount, Coins, N1)) → WAYS_IN(NewAmount, .(s(C), Coins))
WAYS_IN(Amount, .(s(C), Coins)) → U4¹(Amount, C, Coins, =_in(Amount))
U4¹(Amount, C, Coins, =_out(Amount, s(X))) → U9¹(Amount, C, Coins, plus_in(Amount))
U4¹(Amount, C, Coins, =_out(Amount, s(X))) → U5¹(Amount, C, Coins, plus_in(s(C)))
U5¹(Amount, C, Coins, plus_out(s(C), NewAmount, Amount)) → U6¹(Amount, C, Coins, NewAmount, ways_in(Amount, Coins))
U5¹(Amount, C, Coins, plus_out(s(C), NewAmount, Amount)) → WAYS_IN(Amount, Coins)

The TRS R consists of the following rules:

ways_in(Amount, .(s(C), Coins)) → U4(Amount, C, Coins, =_in(Amount))
=_in(X) → =_out(X, X)
U4(Amount, C, Coins, =_out(Amount, s(X))) → U9(Amount, C, Coins, plus_in(Amount))
plus_in(s(X)) → U3(X, plus_in(X))
plus_in(0) → U2(nat_in)
nat_in → U1(nat_in)
nat_in → nat_out(0)
U1(nat_out(X)) → nat_out(s(X))
U2(nat_out(X)) → plus_out(0, X, X)
U3(X, plus_out(X, Y, Z)) → plus_out(s(X), Y, s(Z))
U9(Amount, C, Coins, plus_out(Amount, s(X1), s(C))) → U10(Amount, C, Coins, ways_in(Amount, Coins))
ways_in(X, []) → ways_out(X, [], 0)
ways_in(0, X) → ways_out(0, X, s(0))
U10(Amount, C, Coins, ways_out(Amount, Coins, N)) → ways_out(Amount, .(s(C), Coins), N)
U4(Amount, C, Coins, =_out(Amount, s(X))) → U5(Amount, C, Coins, plus_in(s(C)))
U5(Amount, C, Coins, plus_out(s(C), NewAmount, Amount)) → U6(Amount, C, Coins, NewAmount, ways_in(Amount, Coins))
U6(Amount, C, Coins, NewAmount, ways_out(Amount, Coins, N1)) → U7(Amount, C, Coins, N1, ways_in(NewAmount, .(s(C), Coins)))
U7(Amount, C, Coins, N1, ways_out(NewAmount, .(s(C), Coins), N2)) → U8(Amount, C, Coins, plus_in(N1))
U8(Amount, C, Coins, plus_out(N1, N2, N)) → ways_out(Amount, .(s(C), Coins), N)

The set Q consists of the following terms:

ways_in(x0, x1)
=_in(x0)
U4(x0, x1, x2, x3)
plus_in(x0)
nat_in
U1(x0)
U2(x0)
U3(x0, x1)
U9(x0, x1, x2, x3)
U10(x0, x1, x2, x3)
U5(x0, x1, x2, x3)
U6(x0, x1, x2, x3, x4)
U7(x0, x1, x2, x3, x4)
U8(x0, x1, x2, x3)

We have to consider all (P,Q,R)-chains.
By rewriting [15] the rule WAYS_IN(Amount, .(s(C), Coins)) → U4¹(Amount, C, Coins, =_in(Amount)) at position [3] we obtained the following new rules:

WAYS_IN(Amount, .(s(C), Coins)) → U4¹(Amount, C, Coins, =_out(Amount, Amount))

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

U9¹(Amount, C, Coins, plus_out(Amount, s(X1), s(C))) → WAYS_IN(Amount, Coins)
WAYS_IN(Amount, .(s(C), Coins)) → U4¹(Amount, C, Coins, =_out(Amount, Amount))
U6¹(Amount, C, Coins, NewAmount, ways_out(Amount, Coins, N1)) → WAYS_IN(NewAmount, .(s(C), Coins))
U4¹(Amount, C, Coins, =_out(Amount, s(X))) → U9¹(Amount, C, Coins, plus_in(Amount))
U4¹(Amount, C, Coins, =_out(Amount, s(X))) → U5¹(Amount, C, Coins, plus_in(s(C)))
U5¹(Amount, C, Coins, plus_out(s(C), NewAmount, Amount)) → U6¹(Amount, C, Coins, NewAmount, ways_in(Amount, Coins))
U5¹(Amount, C, Coins, plus_out(s(C), NewAmount, Amount)) → WAYS_IN(Amount, Coins)

The TRS R consists of the following rules:

ways_in(Amount, .(s(C), Coins)) → U4(Amount, C, Coins, =_in(Amount))
=_in(X) → =_out(X, X)
U4(Amount, C, Coins, =_out(Amount, s(X))) → U9(Amount, C, Coins, plus_in(Amount))
plus_in(s(X)) → U3(X, plus_in(X))
plus_in(0) → U2(nat_in)
nat_in → U1(nat_in)
nat_in → nat_out(0)
U1(nat_out(X)) → nat_out(s(X))
U2(nat_out(X)) → plus_out(0, X, X)
U3(X, plus_out(X, Y, Z)) → plus_out(s(X), Y, s(Z))
U9(Amount, C, Coins, plus_out(Amount, s(X1), s(C))) → U10(Amount, C, Coins, ways_in(Amount, Coins))
ways_in(X, []) → ways_out(X, [], 0)
ways_in(0, X) → ways_out(0, X, s(0))
U10(Amount, C, Coins, ways_out(Amount, Coins, N)) → ways_out(Amount, .(s(C), Coins), N)
U4(Amount, C, Coins, =_out(Amount, s(X))) → U5(Amount, C, Coins, plus_in(s(C)))
U5(Amount, C, Coins, plus_out(s(C), NewAmount, Amount)) → U6(Amount, C, Coins, NewAmount, ways_in(Amount, Coins))
U6(Amount, C, Coins, NewAmount, ways_out(Amount, Coins, N1)) → U7(Amount, C, Coins, N1, ways_in(NewAmount, .(s(C), Coins)))
U7(Amount, C, Coins, N1, ways_out(NewAmount, .(s(C), Coins), N2)) → U8(Amount, C, Coins, plus_in(N1))
U8(Amount, C, Coins, plus_out(N1, N2, N)) → ways_out(Amount, .(s(C), Coins), N)

The set Q consists of the following terms:

ways_in(x0, x1)
=_in(x0)
U4(x0, x1, x2, x3)
plus_in(x0)
nat_in
U1(x0)
U2(x0)
U3(x0, x1)
U9(x0, x1, x2, x3)
U10(x0, x1, x2, x3)
U5(x0, x1, x2, x3)
U6(x0, x1, x2, x3, x4)
U7(x0, x1, x2, x3, x4)
U8(x0, x1, x2, x3)

We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule U4¹(Amount, C, Coins, =_out(Amount, s(X))) → U9¹(Amount, C, Coins, plus_in(Amount)) we obtained the following new rules:

U4¹(s(x3), z1, z2, =_out(s(x3), s(x3))) → U9¹(s(x3), z1, z2, plus_in(s(x3)))

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Instantiation

                              ↳ QDP

                                ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

U4¹(s(x3), z1, z2, =_out(s(x3), s(x3))) → U9¹(s(x3), z1, z2, plus_in(s(x3)))
U9¹(Amount, C, Coins, plus_out(Amount, s(X1), s(C))) → WAYS_IN(Amount, Coins)
U6¹(Amount, C, Coins, NewAmount, ways_out(Amount, Coins, N1)) → WAYS_IN(NewAmount, .(s(C), Coins))
WAYS_IN(Amount, .(s(C), Coins)) → U4¹(Amount, C, Coins, =_out(Amount, Amount))
U4¹(Amount, C, Coins, =_out(Amount, s(X))) → U5¹(Amount, C, Coins, plus_in(s(C)))
U5¹(Amount, C, Coins, plus_out(s(C), NewAmount, Amount)) → U6¹(Amount, C, Coins, NewAmount, ways_in(Amount, Coins))
U5¹(Amount, C, Coins, plus_out(s(C), NewAmount, Amount)) → WAYS_IN(Amount, Coins)

The TRS R consists of the following rules:

ways_in(Amount, .(s(C), Coins)) → U4(Amount, C, Coins, =_in(Amount))
=_in(X) → =_out(X, X)
U4(Amount, C, Coins, =_out(Amount, s(X))) → U9(Amount, C, Coins, plus_in(Amount))
plus_in(s(X)) → U3(X, plus_in(X))
plus_in(0) → U2(nat_in)
nat_in → U1(nat_in)
nat_in → nat_out(0)
U1(nat_out(X)) → nat_out(s(X))
U2(nat_out(X)) → plus_out(0, X, X)
U3(X, plus_out(X, Y, Z)) → plus_out(s(X), Y, s(Z))
U9(Amount, C, Coins, plus_out(Amount, s(X1), s(C))) → U10(Amount, C, Coins, ways_in(Amount, Coins))
ways_in(X, []) → ways_out(X, [], 0)
ways_in(0, X) → ways_out(0, X, s(0))
U10(Amount, C, Coins, ways_out(Amount, Coins, N)) → ways_out(Amount, .(s(C), Coins), N)
U4(Amount, C, Coins, =_out(Amount, s(X))) → U5(Amount, C, Coins, plus_in(s(C)))
U5(Amount, C, Coins, plus_out(s(C), NewAmount, Amount)) → U6(Amount, C, Coins, NewAmount, ways_in(Amount, Coins))
U6(Amount, C, Coins, NewAmount, ways_out(Amount, Coins, N1)) → U7(Amount, C, Coins, N1, ways_in(NewAmount, .(s(C), Coins)))
U7(Amount, C, Coins, N1, ways_out(NewAmount, .(s(C), Coins), N2)) → U8(Amount, C, Coins, plus_in(N1))
U8(Amount, C, Coins, plus_out(N1, N2, N)) → ways_out(Amount, .(s(C), Coins), N)

The set Q consists of the following terms:

ways_in(x0, x1)
=_in(x0)
U4(x0, x1, x2, x3)
plus_in(x0)
nat_in
U1(x0)
U2(x0)
U3(x0, x1)
U9(x0, x1, x2, x3)
U10(x0, x1, x2, x3)
U5(x0, x1, x2, x3)
U6(x0, x1, x2, x3, x4)
U7(x0, x1, x2, x3, x4)
U8(x0, x1, x2, x3)

We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule U4¹(Amount, C, Coins, =_out(Amount, s(X))) → U5¹(Amount, C, Coins, plus_in(s(C))) we obtained the following new rules:

U4¹(s(x3), z1, z2, =_out(s(x3), s(x3))) → U5¹(s(x3), z1, z2, plus_in(s(z1)))

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Instantiation

                              ↳ QDP

                                ↳ Instantiation

                                  ↳ QDP

                                    ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

U9¹(Amount, C, Coins, plus_out(Amount, s(X1), s(C))) → WAYS_IN(Amount, Coins)
U4¹(s(x3), z1, z2, =_out(s(x3), s(x3))) → U9¹(s(x3), z1, z2, plus_in(s(x3)))
WAYS_IN(Amount, .(s(C), Coins)) → U4¹(Amount, C, Coins, =_out(Amount, Amount))
U6¹(Amount, C, Coins, NewAmount, ways_out(Amount, Coins, N1)) → WAYS_IN(NewAmount, .(s(C), Coins))
U5¹(Amount, C, Coins, plus_out(s(C), NewAmount, Amount)) → U6¹(Amount, C, Coins, NewAmount, ways_in(Amount, Coins))
U4¹(s(x3), z1, z2, =_out(s(x3), s(x3))) → U5¹(s(x3), z1, z2, plus_in(s(z1)))
U5¹(Amount, C, Coins, plus_out(s(C), NewAmount, Amount)) → WAYS_IN(Amount, Coins)

The TRS R consists of the following rules:

ways_in(Amount, .(s(C), Coins)) → U4(Amount, C, Coins, =_in(Amount))
=_in(X) → =_out(X, X)
U4(Amount, C, Coins, =_out(Amount, s(X))) → U9(Amount, C, Coins, plus_in(Amount))
plus_in(s(X)) → U3(X, plus_in(X))
plus_in(0) → U2(nat_in)
nat_in → U1(nat_in)
nat_in → nat_out(0)
U1(nat_out(X)) → nat_out(s(X))
U2(nat_out(X)) → plus_out(0, X, X)
U3(X, plus_out(X, Y, Z)) → plus_out(s(X), Y, s(Z))
U9(Amount, C, Coins, plus_out(Amount, s(X1), s(C))) → U10(Amount, C, Coins, ways_in(Amount, Coins))
ways_in(X, []) → ways_out(X, [], 0)
ways_in(0, X) → ways_out(0, X, s(0))
U10(Amount, C, Coins, ways_out(Amount, Coins, N)) → ways_out(Amount, .(s(C), Coins), N)
U4(Amount, C, Coins, =_out(Amount, s(X))) → U5(Amount, C, Coins, plus_in(s(C)))
U5(Amount, C, Coins, plus_out(s(C), NewAmount, Amount)) → U6(Amount, C, Coins, NewAmount, ways_in(Amount, Coins))
U6(Amount, C, Coins, NewAmount, ways_out(Amount, Coins, N1)) → U7(Amount, C, Coins, N1, ways_in(NewAmount, .(s(C), Coins)))
U7(Amount, C, Coins, N1, ways_out(NewAmount, .(s(C), Coins), N2)) → U8(Amount, C, Coins, plus_in(N1))
U8(Amount, C, Coins, plus_out(N1, N2, N)) → ways_out(Amount, .(s(C), Coins), N)

The set Q consists of the following terms:

ways_in(x0, x1)
=_in(x0)
U4(x0, x1, x2, x3)
plus_in(x0)
nat_in
U1(x0)
U2(x0)
U3(x0, x1)
U9(x0, x1, x2, x3)
U10(x0, x1, x2, x3)
U5(x0, x1, x2, x3)
U6(x0, x1, x2, x3, x4)
U7(x0, x1, x2, x3, x4)
U8(x0, x1, x2, x3)

We have to consider all (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

U4¹(s(x3), z1, z2, =_out(s(x3), s(x3))) → U9¹(s(x3), z1, z2, plus_in(s(x3)))
U5¹(Amount, C, Coins, plus_out(s(C), NewAmount, Amount)) → WAYS_IN(Amount, Coins)

The remaining pairs can at least be oriented weakly.

U9¹(Amount, C, Coins, plus_out(Amount, s(X1), s(C))) → WAYS_IN(Amount, Coins)
WAYS_IN(Amount, .(s(C), Coins)) → U4¹(Amount, C, Coins, =_out(Amount, Amount))
U6¹(Amount, C, Coins, NewAmount, ways_out(Amount, Coins, N1)) → WAYS_IN(NewAmount, .(s(C), Coins))
U5¹(Amount, C, Coins, plus_out(s(C), NewAmount, Amount)) → U6¹(Amount, C, Coins, NewAmount, ways_in(Amount, Coins))
U4¹(s(x3), z1, z2, =_out(s(x3), s(x3))) → U5¹(s(x3), z1, z2, plus_in(s(z1)))

Used ordering: Polynomial interpretation [25]:

POL(.(x₁, x₂)) = 1 + x₂
POL(0) = 0
POL(=_in(x₁)) = 0
POL(=_out(x₁, x₂)) = 0
POL(U1(x₁)) = 0
POL(U10(x₁, x₂, x₃, x₄)) = 0
POL(U2(x₁)) = 0
POL(U3(x₁, x₂)) = 0
POL(U4(x₁, x₂, x₃, x₄)) = 0
POL(U4¹(x₁, x₂, x₃, x₄)) = 1 + x₃
POL(U5(x₁, x₂, x₃, x₄)) = 0
POL(U5¹(x₁, x₂, x₃, x₄)) = 1 + x₁ + x₃
POL(U6(x₁, x₂, x₃, x₄, x₅)) = 0
POL(U6¹(x₁, x₂, x₃, x₄, x₅)) = 1 + x₃
POL(U7(x₁, x₂, x₃, x₄, x₅)) = 0
POL(U8(x₁, x₂, x₃, x₄)) = 0
POL(U9(x₁, x₂, x₃, x₄)) = 0
POL(U9¹(x₁, x₂, x₃, x₄)) = x₃
POL(WAYS_IN(x₁, x₂)) = x₂
POL([]) = 0
POL(nat_in) = 0
POL(nat_out(x₁)) = 0
POL(plus_in(x₁)) = 0
POL(plus_out(x₁, x₂, x₃)) = 0
POL(s(x₁)) = 0
POL(ways_in(x₁, x₂)) = 0
POL(ways_out(x₁, x₂, x₃)) = 0

The following usable rules [17] were oriented: none

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Instantiation

                              ↳ QDP

                                ↳ Instantiation

                                  ↳ QDP

                                    ↳ QDPOrderProof

                                      ↳ QDP

                                        ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

U9¹(Amount, C, Coins, plus_out(Amount, s(X1), s(C))) → WAYS_IN(Amount, Coins)
U6¹(Amount, C, Coins, NewAmount, ways_out(Amount, Coins, N1)) → WAYS_IN(NewAmount, .(s(C), Coins))
WAYS_IN(Amount, .(s(C), Coins)) → U4¹(Amount, C, Coins, =_out(Amount, Amount))
U5¹(Amount, C, Coins, plus_out(s(C), NewAmount, Amount)) → U6¹(Amount, C, Coins, NewAmount, ways_in(Amount, Coins))
U4¹(s(x3), z1, z2, =_out(s(x3), s(x3))) → U5¹(s(x3), z1, z2, plus_in(s(z1)))

The TRS R consists of the following rules:

ways_in(Amount, .(s(C), Coins)) → U4(Amount, C, Coins, =_in(Amount))
=_in(X) → =_out(X, X)
U4(Amount, C, Coins, =_out(Amount, s(X))) → U9(Amount, C, Coins, plus_in(Amount))
plus_in(s(X)) → U3(X, plus_in(X))
plus_in(0) → U2(nat_in)
nat_in → U1(nat_in)
nat_in → nat_out(0)
U1(nat_out(X)) → nat_out(s(X))
U2(nat_out(X)) → plus_out(0, X, X)
U3(X, plus_out(X, Y, Z)) → plus_out(s(X), Y, s(Z))
U9(Amount, C, Coins, plus_out(Amount, s(X1), s(C))) → U10(Amount, C, Coins, ways_in(Amount, Coins))
ways_in(X, []) → ways_out(X, [], 0)
ways_in(0, X) → ways_out(0, X, s(0))
U10(Amount, C, Coins, ways_out(Amount, Coins, N)) → ways_out(Amount, .(s(C), Coins), N)
U4(Amount, C, Coins, =_out(Amount, s(X))) → U5(Amount, C, Coins, plus_in(s(C)))
U5(Amount, C, Coins, plus_out(s(C), NewAmount, Amount)) → U6(Amount, C, Coins, NewAmount, ways_in(Amount, Coins))
U6(Amount, C, Coins, NewAmount, ways_out(Amount, Coins, N1)) → U7(Amount, C, Coins, N1, ways_in(NewAmount, .(s(C), Coins)))
U7(Amount, C, Coins, N1, ways_out(NewAmount, .(s(C), Coins), N2)) → U8(Amount, C, Coins, plus_in(N1))
U8(Amount, C, Coins, plus_out(N1, N2, N)) → ways_out(Amount, .(s(C), Coins), N)

The set Q consists of the following terms:

ways_in(x0, x1)
=_in(x0)
U4(x0, x1, x2, x3)
plus_in(x0)
nat_in
U1(x0)
U2(x0)
U3(x0, x1)
U9(x0, x1, x2, x3)
U10(x0, x1, x2, x3)
U5(x0, x1, x2, x3)
U6(x0, x1, x2, x3, x4)
U7(x0, x1, x2, x3, x4)
U8(x0, x1, x2, x3)

We have to consider all (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Instantiation

                              ↳ QDP

                                ↳ Instantiation

                                  ↳ QDP

                                    ↳ QDPOrderProof

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

WAYS_IN(Amount, .(s(C), Coins)) → U4¹(Amount, C, Coins, =_out(Amount, Amount))
U6¹(Amount, C, Coins, NewAmount, ways_out(Amount, Coins, N1)) → WAYS_IN(NewAmount, .(s(C), Coins))
U5¹(Amount, C, Coins, plus_out(s(C), NewAmount, Amount)) → U6¹(Amount, C, Coins, NewAmount, ways_in(Amount, Coins))
U4¹(s(x3), z1, z2, =_out(s(x3), s(x3))) → U5¹(s(x3), z1, z2, plus_in(s(z1)))

The TRS R consists of the following rules:

ways_in(Amount, .(s(C), Coins)) → U4(Amount, C, Coins, =_in(Amount))
=_in(X) → =_out(X, X)
U4(Amount, C, Coins, =_out(Amount, s(X))) → U9(Amount, C, Coins, plus_in(Amount))
plus_in(s(X)) → U3(X, plus_in(X))
plus_in(0) → U2(nat_in)
nat_in → U1(nat_in)
nat_in → nat_out(0)
U1(nat_out(X)) → nat_out(s(X))
U2(nat_out(X)) → plus_out(0, X, X)
U3(X, plus_out(X, Y, Z)) → plus_out(s(X), Y, s(Z))
U9(Amount, C, Coins, plus_out(Amount, s(X1), s(C))) → U10(Amount, C, Coins, ways_in(Amount, Coins))
ways_in(X, []) → ways_out(X, [], 0)
ways_in(0, X) → ways_out(0, X, s(0))
U10(Amount, C, Coins, ways_out(Amount, Coins, N)) → ways_out(Amount, .(s(C), Coins), N)
U4(Amount, C, Coins, =_out(Amount, s(X))) → U5(Amount, C, Coins, plus_in(s(C)))
U5(Amount, C, Coins, plus_out(s(C), NewAmount, Amount)) → U6(Amount, C, Coins, NewAmount, ways_in(Amount, Coins))
U6(Amount, C, Coins, NewAmount, ways_out(Amount, Coins, N1)) → U7(Amount, C, Coins, N1, ways_in(NewAmount, .(s(C), Coins)))
U7(Amount, C, Coins, N1, ways_out(NewAmount, .(s(C), Coins), N2)) → U8(Amount, C, Coins, plus_in(N1))
U8(Amount, C, Coins, plus_out(N1, N2, N)) → ways_out(Amount, .(s(C), Coins), N)

The set Q consists of the following terms:

ways_in(x0, x1)
=_in(x0)
U4(x0, x1, x2, x3)
plus_in(x0)
nat_in
U1(x0)
U2(x0)
U3(x0, x1)
U9(x0, x1, x2, x3)
U10(x0, x1, x2, x3)
U5(x0, x1, x2, x3)
U6(x0, x1, x2, x3, x4)
U7(x0, x1, x2, x3, x4)
U8(x0, x1, x2, x3)

We have to consider all (P,Q,R)-chains.